\documentclass{article} 
\usepackage{url} 
\usepackage{hyperref}
\usepackage{stmaryrd}
\usepackage{manfnt}
\usepackage{fullpage}
\usepackage{proof}
\usepackage{savesym}
\usepackage{amssymb} 
%% \savesymbol{mathfrak}
%\usepackage{MnSymbol} Overall mnsymbol is depressing.
%\restoresymbol{MN}{mathfrak}
\usepackage{xcolor} 
%\usepackage{mathrsfs}
\usepackage{amsmath, amsthm}
%\usepackage{diagrams}
\makeatletter
\newsavebox{\@brx}
\newcommand{\llangle}[1][]{\savebox{\@brx}{\(\m@th{#1\langle}\)}%
  \mathopen{\copy\@brx\kern-0.6\wd\@brx\usebox{\@brx}}}
\newcommand{\rrangle}[1][]{\savebox{\@brx}{\(\m@th{#1\rangle}\)}%
  \mathclose{\copy\@brx\kern-0.6\wd\@brx\usebox{\@brx}}}
\makeatother

\definecolor{light-gray}{gray}{0.86}
\newcommand{\gray}[1]{\colorbox{light-gray}{#1}}
\newtheorem{prop}{Proposition}
\newtheorem{definition}{Definition}
\newtheorem{corollary}{Corollary}
\newtheorem{lemma}{Lemma}
\newtheorem{theorem}{Theorem}


\newcommand{\mlstep}[1]{\twoheadrightarrow_{\underline{#1}}}
\newcommand{\lstep}[1]{\to_{\underline{#1}}}
\newcommand{\mstep}[1]{\twoheadrightarrow_{#1}}
\newcommand{\ep}[0]{\epsilon} 
\newcommand{\nil}[0]{\mathsf{nil}} 
\newcommand{\cons}[0]{\mathsf{cons}} 
\newcommand{\vecc}[0]{\mathsf{vec}} 
\newcommand{\suc}[0]{\mathsf{S}} 
\newcommand{\pred}[0]{\mathsf{Pred}} 
\newcommand{\app}[0]{\mathsf{app}} 
\newcommand{\add}[0]{\mathsf{add}} 
\newcommand{\interp}[1]{\llbracket #1 \rrbracket} 
\newcommand{\intern}[1]{\llbracket #1 \rrbracket^{-1}} 
\newcommand{\self}[0]{\mathbf{S}} 
\newcommand{\selfstar}[0]{\mathsf{Selfstar}} 
\newcommand{\systemg}[0]{\mathfrak{G}} 
\newcommand{\fomega}[0]{\mathbf{F}_{\omega}} 
\newcommand{\nat}[0]{\mathsf{Nat}} 

%% \newcommand{\mlstep}[1]{\twoheadrightarrow_{\underline{#1}}}
%% \newcommand{\lstep}[1]{\to_{\underline{#1}}}
%% \newcommand{\mstep}[1]{\twoheadrightarrow_{#1}}
%% \newcommand{\ep}[0]{\epsilon} 
%% \newcommand{\nil}[0]{\mathsf{nil}} 
%% \newcommand{\cons}[0]{\mathsf{cons}} 
%% \newcommand{\vecc}[0]{\mathsf{vec}} 
%% \newcommand{\suc}[0]{\mathsf{S}} 
%% \newcommand{\app}[0]{\mathsf{app}} 
%% \newcommand{\interp}[1]{\llbracket #1 \rrbracket} 
%% \newcommand{\intern}[1]{\llangle #1 \rrangle} 
%% \newcommand*\template[1]{\(\langle\)#1\(\rangle\)}
%% \newarrowfiller{dasheq} {==}{==}{==}{==}
%% \newarrow {Mapsto} |--->
%% \newarrow {Line} -----
%% \newarrow {Implies} ===={=>}
%% \newarrow {EImplies} {}{dasheq}{}{dasheq}{=>}
%% \newarrow {Onto} ----{>>}
%% \newarrow {Dashto}{}{dash}{}{dash}{>}
%% \newarrow {Dashtoo}{}{dash}{}{dash}{>>}

%% \newtheorem{prop}{Proposition}
%% \newtheorem{definition}{Definition}
%% \newtheorem{corollary}{Corollary}
%% \newtheorem{lemma}{Lemma}
%% \newtheorem{theorem}{Theorem}
\definecolor{light-gray}{gray}{0.86}

\begin{document}
%\pagestyle{empty}
\title{Lambda Encoding with Comprehension}
\author{Peng Fu \\
Computer Science, The University of Iowa}
\date{\today}


\maketitle \thispagestyle{empty}

\section{Introduction}
In this chapter, we will see iota-binder from a different perspective. Instead of viewing iota-binder as a type construct, we view it as a set-forming construct. So if $F[x]$ is a formula containing a free term variable $x$ , then $\iota x.F[x]$ describes a set of terms $t$, which satisfies the formula, i.e. $ t \in \iota x.F[x] $ iff $ F[t]$. Recalled that in $\selfstar$ and $\self$, we have $\vdash t : \iota x.T$ iff $\vdash t:[t/x]T$. If we compare $t \in \iota x.F[x]$ with $\vdash t: \iota x.T$, we observe that there is a similarity between the meta-level typing relation (denoted by ``$:$'') and the set membership notation ``$\in$'', which lies in the object logic. This observation is inspired from our earlier work on internalization \cite{fu2011framework}. Right now we are being informal, because it is hard to draw a connection between $F[t]$ and $\vdash t:[t/x]T$, since equating $t \in F[t]$ with $F[t]$ violates the grammatical structure of the logic. Furthermore, one can not na\"ively views self type as formula. Suppose both $\iota x.T$ and $T$ are corresponding to formulas, we know that for the formula $F[x]$, the $\iota x.F[x]$ is representing a set, not a formula, so it is again incoherent to equates $\iota x.F[x]$ with $\iota x.T$. Nonetheless, the observation above motivates us to investigate iota-binder from a pure logical perspective. 

Another source of inspiration of our work in this Chapter is from Hatcher's formulation of Frege's logic \cite{hatcher:1982}. Hatcher presented Frege's system \cite{frege1967basic} in modern notations, i.e. a logic with basic set-like construct and comprehension axiom. He showed how to prove all of Peano's axioms in Frege's system. Dispite Frege's system itself is inconsistent, the development of Peano's axioms, especially the derivation of induction principle is remarkable and should be emphasis over the inconsistency. In fact, later we can see the derivation of induction principle follows the spirit of Frege.   

We first present Frege's System $\mathfrak{F}$ (section \ref{frege}), to motivate our construction of arithmetic with lambda calculus. Then we give a formulation of second order theory of lambda calculus based on 
iota-binder $\iota$ and epsilon relation $\ep$, we call it $\mathfrak{G}$ (section \ref{sysg}). There are at least three similar systems, namely, Girard's formulation of $\mathbf{HA}_2$ \`a la Takeuti \cite{Girard:1989}, Krivine's $\mathbf{FA}_2$ \cite{krivine2002lambda} and Takeuti's second order logic \cite{takeuti1975proof}. There are two major differences between $\systemg$ and these systems, the first one is that the domain of individuals of $\systemg$ is lambda terms instead of primitive notion of numbers. The second one is that $\systemg$ has $(\ep, \iota)$-notation, namely, set-abstraction and membership relation are explict in the object language. Thus comprehension axiom is needed in $\systemg$. While the other systems use predication instead of membership relation, and set-abstraction is implicit at the meta-level, the comprehension axiom is admissible by performing substitution. The second difference is subtle and has significant implications, as we shall see in section \ref{internal}, we can define a notion of polymorphic-dependent typing within $\systemg$, which benefits from the facts that $\systemg$ adimits $(\ep, \iota)$-notation.  

We prove all of Peano's axioms in section \ref{peano}. We enrich the reduction on lambda term with $\eta$-and $\Omega$-reductions, then we are able to show that the member of the inductively 
defined sets such as $\nat$ is terminating with respect to \textit{head beta-reduction} (section \ref{prog}). Finally, we show the notion of Leibniz equality in $\systemg$ is \textit{faithful} to the conversions in lambda calculus (section \ref{leibniz}). 
 

\section{Frege's System $\mathfrak{F}$}
\label{frege}

Certain inconsistent systems and their corresponding antinomies are invaluable, because not only the antinomies can be served as criterions for maintaining consistency, but also, perhaps more importantly, they gives us examples to see how to reconstruct a large part of mathematics within these systems. Frege's system (\`a la Hatcher) belongs to this category. In fact, $\systemg$ is inspired by the Fregean construction of numbers. We formalize a intuitionistic version of Frege's system $\mathfrak{F}$ in the form of sequent calculus, and then we show how to derive basic arithmetic with $\mathfrak{F}$ and see how the antinomy arises. 

\begin{definition}[Syntax]
\

\noindent \textit{Domain Terms/Set} $a, b, s \ :: = \ x \ | \ \iota x.F$

\noindent \textit{Formula} $F \ ::= \bot \ | \ s \ep s' \ | \ \ F_1 \to F_2 \ | \ \forall x.F \ | \ F \wedge F'$

\noindent \textit{Context} $\Gamma \ :: = \ \cdot \ | \ \Gamma, F$

\end{definition} 

We identify four syntactical categories in $\mathfrak{F}$, namely, \textit{domain terms}, \textit{set} and \textit{formula}. Note that \textit{set} in this chapter is just a name for a syntactical category, we should not confused the notion of set in this chapter with the ``set'' in $\mathbf{ZF}$. Also, the notion of set coincides with the notion of domain terms in $\mathfrak{F}$.  

\begin{definition}[Deduction Rules]

  \

  \

\begin{tabular}{lll}
    
\infer{\Gamma \vdash F}{F \in \Gamma}

&
\infer{\Gamma \vdash  F_2}{\Gamma \vdash 
F_1 &  F_1 = F_2}

&

\infer{\Gamma \vdash \forall x.F}
{\Gamma \vdash  F &  x \notin \mathrm{FV}(\Gamma)}

\\
\\
\infer{\Gamma \vdash [s/x]F}{\Gamma
\vdash \forall x.F}

&

\infer{\Gamma \vdash F_1\to F_2}
{\Gamma, F_1 \vdash F_2}

&

\infer{\Gamma \vdash  F_2}{\Gamma
\vdash F_1 \to F_2 & \Gamma \vdash  F_1}
\\
\\

\infer{\Gamma \vdash F_i}{\Gamma
\vdash  F_1 \wedge F_2 }

&

\infer{\Gamma \vdash  F_1 \wedge F_2}{\Gamma
\vdash F_1 & \Gamma \vdash  F_2 }

\end{tabular}

\end{definition}

$F_1 = F_2$ is specified by the comprehension axiom. 

\begin{definition}[Comprehension]
$s \ep (\iota x.F) = [s/x]F$
\end{definition}

Comprehension axiom is essential for Fregean number construction. The definition of 
number, the induction principle for numbers rely on comprehension. 
Because the notion domain terms and set coincide, with comprehension axiom, $\mathfrak{F}$ is inconsistent. There are three major ways to avoid the antinomy, namely,  Russell's type theory \cite{whitehead1927principia}, Quine's new foundation \cite{quine1937new} and Zermelo's $\mathbf{ZF}$ \cite{zermelo1908untersuchungen}. In next section, we present System $\systemg$, which separates the notion of domain terms and set, thus is in the spirit of Quine's stratefication.

\begin{definition}[Equality]
  $a = b := \forall z. (z \ep a \equiv z \ep b)$.
\end{definition}

For convenient, we write $a \equiv b$ to denote $ a \to b . \wedge . b \to a$. We also write $a \not = b$
for $a = b \to \bot$, $\exists a. A $ for $ (\forall a.(A \to \bot)) \to \bot$. Now we can proceed to construct a na\"ive set theory in $\mathfrak{F}$.

\begin{definition}[Na\"ive Set Theory]
\

  $\Lambda := \iota x.(x  = x \to \bot)$.

  $\{ b\} := \iota y. y = b$

  $\bar{c} := \iota y. (y \ep c \to \bot)$.

  $ a \cap b := \iota z. (z \ep a \wedge z \ep b)$

 $ a \cup b := \iota z. (z \ep a \to \bot . \wedge . z \ep b \to \bot) \to \bot$
\end{definition}

\begin{theorem}
\

  $\vdash \forall x.(x = x)$

  $\vdash \forall x.(x \ep \Lambda \to \bot)$.
\end{theorem}

We can take $x \ep \Lambda$ as our notion of contradictory because $x \ep \Lambda$ implies $\bot$. We now can develop an elementary number theory in $\mathfrak{F}$. 

\begin{definition}[Fregean Numbers]
\

  $N := \iota x. \forall c.(\forall y.(y \ep c \to S y \ep c)) \to 0 \ep c \to x \ep c$.

  $0 := \{ \Lambda \}$.

  $S\ a := \iota y. \exists z.(z \ep y . \wedge . (y \cap \overline{\{z\}}) \ep a )$.
\end{definition}

\begin{theorem}
  \

$\vdash 0 \ep N$.
\end{theorem}
\begin{proof}
  We want to prove $\forall c.(\forall y.(y \ep c \to S y \ep c)) \to 0 \ep c \to 0 \ep c$. Assume $\forall y.(y \ep c \to S y \ep c)$ and $0 \ep c$, we want to show $0 \ep c$, which
  is obvious\footnote{Observe that the lambda term for the proof is Church numberal zero
$\lambda s.\lambda z.z$.}. 
\end{proof}

\begin{theorem}
  $\vdash \forall y. (y \ep N \to S y \ep N)$.
\end{theorem}
\begin{proof}
Assume $y \ep N$, we want to show $S y \ep N$. By comprehension, we want to show $\forall c.(\forall y.(y \ep c \to S y \ep c)) \to 0 \ep c \to (S y) \ep c$. So we assume $\forall y.(y \ep c \to S y \ep c)$ and $0 \ep c$, we need to show $(S y) \ep c$. We know that $y \ep N$ implies $\forall c.(\forall y.(y \ep c \to S y \ep c)) \to 0 \ep c \to y \ep c$. By modus ponens, we have $y \ep c$. By universal instantiation, we have $y \ep c \to S y \ep c$. So by modus ponens, we have $S y \ep c$. Thus we have the proof\footnote{The lambda term for this proof is Church successor $\lambda n.\lambda s.\lambda z.s (n\ s\ z)$.}.
\end{proof}

\begin{theorem}[Induction Principle]
  $\vdash \forall c.(\forall y.(y \ep c \to S y \ep c)) \to 0 \ep c \to \forall x.(x \ep N \to x \ep c)$.
\end{theorem}
\begin{proof}
 Assume $\forall y.(y \ep c \to S y \ep c), 0 \ep c, x\ep N$. We want to show $x \ep c$. We 
 know $x \ep N$ implies $\forall c.(\forall y.(y \ep c \to S y \ep c)) \to 0 \ep c \to x \ep c$. By modus ponens, we get $x \ep c$\footnote{The lambda term for this proof is iterator $\lambda f.\lambda a.\lambda n.n\ f\ a$.}. 
\end{proof}

We observe that there is an algorithmic interpretation for constructive proof of totality of certain kind of function. For example, the proof of $S$ is total, namely, $\forall y. (y \ep N \to S y \ep N)$, can be encoded as Church numeral's successor $\lambda n.\lambda s.\lambda z. s\ (n \ s\ z)$. This result is already known by Leivant and Krivine \cite{leivant1983reasoning}, \cite{krivine2002lambda}. So one should at least admit there is constructive flavor in Fregean construction of number. Of course, the system itself is inconsistent, i.e. the following formula is provable in system $\mathfrak{F}$: 

Let $A := (\iota u_1. u_1 \not \in u_1) \ep (\iota u_1. u_1 \not \in u_1) = A \to \bot$. So we have $ \vdash A \to \bot$ since $A \vdash A$ and $A \vdash A \to \bot$. Also, $A \to \bot \vdash A \to \bot$ implies $A \to \bot \vdash A$, thus $\vdash (A \to \bot) \to \bot$. By modus ponens, we can derive $\vdash \bot$. It is worthnoting that intuitionistic is irrelavant to prevent inconsistency.

However, as we repeatly emphasis, it is the constructive spirit that we should take upon ourself, the antinomy only serves as a criterion of the boundary. 




\section{System $\mathfrak{G}$}
\label{sysg}

System $\systemg$ is inspired by Frege's $\mathfrak{F}$ and the possibility of understanding the iota-binder as set-abstraction in higher order logic. System $\systemg$ is a \textit{simple} logical system with the $(\ep, \iota)$-notation. 

\begin{definition}
\

\noindent \textit{Formula} $F \ ::= \  X^0 \ | \ t \ep S \ | \ \Pi X^1.F \ | \ \ F_1 \to F_2 \ | \ \forall x.F \ | \ \Pi X^0.F$ 

\noindent \textit{Set} $S \ ::= X^1 \ | \ \iota x.F$

%% \noindent \textit{Morphism} $M \ ::= t \ep S \ | \ \forall x.(x\ep S \to M)$

\noindent \textit{Domain Terms/Pure Lambda Terms} $t \ :: = \ x \ | \ \lambda x.t \ | \ t t'$

%\noindent \textit{Proof Terms} $p \ ::= \ a \ | \ \lambda a .p \ | \ p p'$

\noindent \textit{Context} $\Gamma \ :: = \ \cdot \ | \ \Gamma, F$

%\noindent \textit{Records} $\Delta \ :: = \ \cdot \ | \ \Delta, a: x \ep S$

\end{definition} 

$X^0$ is a formula variable, it represents any formula. $X^1$ is a set variable, it represents any set. $\iota x.F$ is the set formed by the formula $F$. Unlike $\mathfrak{F}$, we separate
the notion of set and domain terms, the domain terms in $\mathfrak{G}$ are pure lambda terms. Set can only occur inside of a formula, they do not have their own rule and identity outside of a formula. Again, please do not confuse the set in this chapter with the set in $\mathbf{ZF}$. $\Pi X^0.F$ is a formula formed by quantifying over formula and $\Pi X^1.F$ is formed by quantifying over set. The notation of $\ep, \iota$ are formal parts of the language of $\systemg$, they are called $(\ep, \iota)$-notation.

\begin{definition}[Deduction Rules]
\

\

\begin{tabular}{lll}
    
\infer{\Gamma \vdash F}{F \in \Gamma}

&
\infer[\textit{Conv}]{\Gamma \vdash F_2}{\Gamma \vdash 
F_1 &  F_1 =_{\beta, \iota} F_2}

&

\infer{\Gamma \vdash \forall x.F}
{\Gamma \vdash F &  x \notin \mathrm{FV}(\Gamma)}

\\
\\
\infer{\Gamma \vdash [t/x]F}{\Gamma
\vdash \forall x.F}
&

\infer{\Gamma \vdash  \Pi X^i.F}
{\Gamma \vdash F & X^i \notin \mathrm{FV}(\Gamma) & i= 0,1}

&
\infer[\textit{Inst0}]{\Gamma \vdash [F'/X^0]F}{\Gamma \vdash \Pi X^0.F}

\\
\\

\infer{\Gamma \vdash F_1\to F_2}
{\Gamma, F_1 \vdash F_2}

&

\infer{\Gamma \vdash F_2}{\Gamma
\vdash  F_1 \to F_2 & \Gamma \vdash F_1}

&


\infer[\textit{Inst1}]{\Gamma \vdash [S/X^1]F}{\Gamma \vdash \Pi X^1.F}

\end{tabular}

\end{definition}

The rule \textit{Inst0} allows us to instantiate $X^0$ with 
any formula, this is what the instantiation does in system \textbf{F}, while the \textit{Inst1} rule allows us to instantiate a set variable $X^1$ with any set $S$.

\begin{definition}[Axioms]
$F_1 =_{\iota,\beta} F_2$ iff one the the following holds.

  \begin{enumerate}
  \item $F_1$ (or $F_2$) is of the form $t \ep (\iota x.F)$ and $F_2$ (or $F_1$) is of the form $[t/x]F$. 
    \item $F_1$ (or $F_2$) contains a term $t$ and $F_2$ (or $F_1$) is obtained from $F_1$ by replacing $t$ with its beta-equivalent term $t'$. 
  \end{enumerate}
\end{definition}

The first axiom corresponds to the comprehension axiom. The second axiom corresponds to 
the axiom of extensionality \cite{hatcher:1982}, it also depends on beta-conversion axiom
in lambda calculus. We know that beta-conversion in lambda calculus is Church-Rosser, thus not every lambda terms are considered equal. The reason we set up axioms through the \textit{Conv} rule is that it will not affect the overall proof tree, a direct consequence is that then 
consistency is easy to prove, as we shall see next. 
 

\subsection{Consistency of System $\systemg$}
We have presented the whole specifications of $\systemg$. Now we show $\systemg$ is consistent, in the sense that not every formula is provable in $\systemg$. To prove consistency, we will first devise a version of $\mathfrak{G}$ with proof term annotation, denoted by $\systemg\lbrack p \rbrack$. Then a forgetful mapping from 
$\mathfrak{G}\lbrack p \rbrack$ to System $\mathbf{F}$ is defined. Finally, any deravable judgement in $\mathfrak{G}\lbrack p \rbrack$ can be mapped to a deravable judgement in System $\mathbf{F}$. Thus we can conclude the proof term for $\systemg\lbrack p \rbrack$ is strongly normalizing and not every formula in $\systemg$ is provable.

\begin{definition}[System $\systemg \lbrack p \rbrack$]
\

\noindent  \textit{Proof Terms} $p \ ::= \ a \ | \ \lambda a .p \ | \ p p'$

\noindent  \textit{Proof Context} $\Gamma \ ::= \ \cdot \ | \ a:F, \Gamma$

\

\begin{tabular}{lll}
    
\infer{\Gamma \vdash p : \forall x.F}
{\Gamma \vdash p: F &  x \notin \mathrm{FV}(\Gamma)}

&
\infer{\Gamma \vdash p : F_2}{\Gamma \vdash p:
F_1 &  F_1 =_{\beta,\iota} F_2}

&
\infer{\Gamma \vdash a:F}{(a:F) \in \Gamma}


\\
\\
\infer{\Gamma \vdash p :[t'/x]F}{\Gamma
\vdash p: \forall x.F}
&

\infer{\Gamma \vdash  p :\Pi X^i.F}
{\Gamma \vdash p: F & X^i \notin \mathrm{FV}(\Gamma) & i= 0,1}

&
\infer{\Gamma \vdash p:[F'/X^0]F}{\Gamma \vdash p: \Pi X^0.F}

\\
\\

\infer{\Gamma \vdash \lambda a.p : F_1\to F_2}
{\Gamma, a:F_1 \vdash p: F_2}

&

\infer{\Gamma \vdash p p':F_2}{\Gamma
\vdash p: F_1 \to F_2 & \Gamma \vdash p': F_1}

&


\infer{\Gamma \vdash p:[S/X^1]F}{\Gamma \vdash p: \Pi X^1.F}

\end{tabular}

\end{definition}

\noindent The proof terms only annotated the introduction and elimination rules of implication. We now define the mapping to System $\mathbf{F}$. 

\begin{definition}
\

\

\begin{tabular}{ll}
  $\phi(X^0) := X$

  &
  
  $\phi(t \ep S) := \phi(S)$
  
  \\
  
  $\phi(F_1 \to F_2) := \phi(F_1) \to \phi(F_2)$
  &
  
  $\phi(\Pi X^0.F) := \Pi X.\phi(F)$

  \\

    $\phi(\Pi X^1.F) := \Pi X.\phi(F)$

  &
  
    $\phi(\forall x.F) := \phi(F)$
  
  \\
   $\phi(X^1) := X$
  
  &
  $\phi(\iota x.F) := \phi(F)$
\end{tabular}
\end{definition}

\noindent Note that the function $\phi$ can be easily extended to the proof context. It maps formula and set in $\systemg\lbrack p \rbrack$ to types in System $\mathbf{F}$.

\begin{lemma}
  \label{eq-phi}
  \
  
  \begin{enumerate}
  \item If $F_1 =_{\beta, \iota} F_2$, then $\phi(F_1) \equiv \phi(F_2)$.
    \item  $\phi(F) \equiv \phi([t'/x]F)$.
      \item $\phi([F'/X^0]F) \equiv [\phi(F')/X]\phi(F)$. 
      \item $\phi([S/X^1]F) \equiv [\phi(S)/X]\phi(F)$. 
        
  \end{enumerate}
\end{lemma}

\noindent The following theorem connects System $\systemg \lbrack p \rbrack$ with System $\mathbf{F}$.

\begin{theorem}
  \label{const}
 If $\Gamma \vdash p:F$ in $\systemg \lbrack p \rbrack$, then $\phi(\Gamma)\vdash p:\phi(F)$ in $\mathbf{F}$.
\end{theorem}

\begin{proof}
  By induction on the derivation of $\Gamma \vdash p:F$.

  \noindent \textbf{Case}: 

  \
  
  \infer{\Gamma \vdash a:F}{(a:F) \in \Gamma}
  
  \noindent By $a:\phi(F)\in \phi(\Gamma)$.

    \noindent \textbf{Case}: 

    \
    
\infer{\Gamma \vdash p : \forall x.F}
{\Gamma \vdash p: F &  x \notin \mathrm{FV}(\Gamma)}

    \noindent By IH, we know that $\phi(\Gamma) \vdash p: \phi(F) \equiv \phi(\forall x.F)$. 
    
      \noindent \textbf{Case}: 

  \

\infer{\Gamma \vdash p : F_2}{\Gamma \vdash p:
F_1 &  F_1 =_{\beta,\iota} F_2}

\noindent By lemma \ref{eq-phi}, we know that $\phi(F_1) \equiv \phi(F_2)$.

  \noindent \textbf{Case}: 

  \

\infer{\Gamma \vdash p :[t'/x]F}{\Gamma
\vdash p: \forall x.F}

\noindent By lemma \ref{eq-phi}, we know that $\phi(\forall x.F) \equiv \phi(F) \equiv \phi([t'/x]F)$. 

  \noindent \textbf{Case}: 

  \

\infer{\Gamma \vdash  p :\Pi X^i.F}
{\Gamma \vdash p: F & X^i \notin \mathrm{FV}(\Gamma) & i= 0,1}

\noindent By IH, we know $\phi(\Gamma) \vdash p:\phi(F)$. And $X \notin \mathrm{FV}(\phi(\Gamma))$, thus $\phi(\Gamma) \vdash p: \Pi X.\phi(F) \equiv \phi(\Pi^i X.F)$.

  \noindent \textbf{Case}: 

  \

\infer{\Gamma \vdash p:[F'/X^0]F}{\Gamma \vdash p: \Pi X^0.F}

\noindent By IH, we know that $\phi(\Gamma) \vdash p: \Pi X.\phi(F)$. Thus $\phi(\Gamma) \vdash p: [\phi(F')/X]\phi(F) \equiv \phi([F'/X^0]F)$. The last equality is by lemma \ref{eq-phi}.

  \noindent \textbf{Case}: 

  \

\infer{\Gamma \vdash \lambda a.p : F_1\to F_2}
{\Gamma, a:F_1 \vdash p: F_2}

\noindent By IH, we know $\phi(\Gamma), a:\phi(F_1) \vdash p: \phi(F_2)$. Thus $\phi(\Gamma) \vdash \lambda a.p: \phi(F_1) \to \phi(F_2)$.

  \noindent \textbf{Case}: 

  \


\infer{\Gamma \vdash p p':F_2}{\Gamma
\vdash p: F_1 \to F_2 & \Gamma \vdash p': F_1}

\noindent By IH, $\phi(\Gamma) \vdash p: \phi(F_1) \to \phi(F_2)$ and $ \phi(\Gamma) \vdash p': \phi(F_1)$. Thus $\phi(\Gamma) \vdash p p':\phi(F_2)$. 

  \noindent \textbf{Case}: 

  \
  
\infer{\Gamma \vdash p:[S/X^1]F}{\Gamma \vdash p: \Pi X^1.F}

\noindent By IH, we know that $\phi(\Gamma) \vdash p: \Pi X.\phi(F)$. Thus $\phi(\Gamma) \vdash p: [\phi(S)/X]\phi(F) \equiv \phi([S/X^1]F)$. The last equality is by lemma \ref{eq-phi}.

\end{proof}

Theorem \ref{const} implies that if $\Gamma \vdash p:F$ in $\systemg\lbrack p \rbrack$, then $p$ is strongly normalizing and that the formlua $\Pi X^0.X$ in $\systemg$ is unprovable. 

\subsection{Preservation Theorem for $\systemg\lbrack p \rbrack$}

We need to establish preservation property for $\systemg\lbrack p \rbrack$ in order to explore more unprovable formulas in $\systemg$. The proof of preservation theorem is an adaption of Barendregt's method for proving preservation for System $\mathbf{F}$ \`a la Curry \cite{Barendregt:92}. 

\begin{definition}[Formula Reduction]
\

\begin{itemize}
  \item $F_1 \to_{\beta} F_2$ if $t_1 =_{\beta} t_2$, $F_1 \equiv F[t_1]$ and $F_2 \equiv F[t_2]$.
    \item $F_1 \to_{\iota} F_2$ if $F_1 \equiv t\ep \iota x.F$ and $F_2 \equiv [t/x]F$.
  \end{itemize}
\end{definition}

\noindent Note that $F[t_1]$ means the lambda term $t_1$ appears inside the formula $F$ and 
$\to_{\beta, \iota}$ denotes $\to_{\beta} \cup \to_{\iota}$. 

\begin{lemma}
  $\to_{\beta, \iota}$ is confluent. 
\end{lemma}
\begin{proof}
  We know that $\to_{\beta}$ and $\to_{\iota}$ are confluent. We also know that $\to_{\beta}$
  commutes with $\to_{\iota}$, so $\to_{\beta, \iota}$ is confluent.
\end{proof}

\begin{definition}[Morphing Relations]
\

  \begin{itemize}
   \item $F_1 \to_i F_2$ if $F_1 \equiv \forall x.F$ and $F_2 \equiv [t/x]F$ for some term
     $t$.
   \item  $F_1 \to_g F_2$ if $F_2 \equiv \forall x.F_1$.

   \item $F_1 \to_I F_2$ if $F_1 \equiv \Pi X^0.F$ and $F_2 \equiv [F'/X^0]F$ for formula
     $F'$.
   \item  $F_1 \to_G F_2$ if $F_2 \equiv \Pi X^0.F_1$.

   \item $F_1 \to_{is} F_2$ if $F_1 \equiv \Pi X^1.F$ and $F_2 \equiv [S/X^1]F$ for some set
     $S$.
   \item  $F_1 \to_{gs} F_2$ if $F_2 \equiv \Pi X^1.F_1$.

  \end{itemize}
\end{definition}

\noindent Let $\twoheadrightarrow_{gi}$ denotes the reflexive and transitive closure of 
$\to_{i,g, I, G, is, gs}$. 

\begin{lemma}
Suppose no free variable of $F$ occurs in $\Gamma$. If $\Gamma \vdash p: F$ and $F \twoheadrightarrow_{gi} F'$, then $\Gamma \vdash p: F'$.
\end{lemma}


\begin{definition}
\

  \begin{tabular}{lll}
  $E_0(\Pi X^0.F) := E_0(F)$
&
  $E_0(X^0) := X^0$

&

 $E_0(F_1\to F_2) := F_1\to F_2$

\\
  $E_0(\Pi X^1.F) := \Pi X^1.F$
&

$E_0(\forall x.F) := \forall x.F$

&

$E_0(t\ep S) := t\ep S$
\end{tabular}
\end{definition}

\begin{definition}
\

  \begin{tabular}{lll}
  $E_1(\Pi X^1.F) := E_1(F)$
&
  $E_1(X^0) := X^0$

&

 $E_1(F_1\to F_2) := F_1\to F_2$

\\
$E_1(t\ep S) := t\ep S$
&

$E_1(\forall x.F) := \forall x.F$

&

  $E_1(\Pi X^0.F) := \Pi X^0.F$

\end{tabular}
\end{definition}

\begin{definition}
\

  \begin{tabular}{lll}
  $G(\Pi X^i.F) := \Pi X^i.F$
&
  $G(X^0) := X^0$

&

 $G(F_1\to F_2) := F_1\to F_2$

\\

$G(\forall x.F) := G(F)$

&
$G(t\ep S) := t\ep S$

\end{tabular}
\end{definition}

\begin{lemma}
  \label{subeg}
  $E_0([F'/X^0]F) \equiv [F''/X^0]E_0(F)$ for some $F''$; $E_1([S/X^1]F) \equiv [S/X^1]E_1(F)$; $G([t/x]F) \equiv [t/x]G(F)$.  
\end{lemma}

\begin{proof}
Proof by induction on the structure of $F$.  
\end{proof}

\begin{lemma}
  \label{termsub}
  If $F \twoheadrightarrow_{i, g} F'$, then there exist a substitution $\delta$ with domain
  of term variables and codomain of terms such that $\delta G(F) \equiv G(F')$.
\end{lemma}

\begin{proof}
  It suffices to consider $ F {\to_{i,g}} F'$.
If $F' \equiv \forall x .F$, then $G(F') \equiv G(F)$.
If $F \equiv \forall x .F_1$ and $F' \equiv [t/x]F_1$, then $G(F) \equiv G(F_1)$. By lemma \ref{subeg}, we know $G(F') \equiv G([t/x]F_1) \equiv [t/x]G(F_1)$. 
\end{proof}

\begin{lemma}
  \label{formsub}
  If $F \twoheadrightarrow_{I, G} F'$, then there exist a substitution $\delta$ with domain
  of formula variables and codomain of formulas such that $\delta E_0(F) \equiv E_0(F')$.
\end{lemma}
\begin{proof}
    It suffices to consider $F {\to_{I,G}} F'$. If $F' \equiv \Pi X^0.F$, then $E_0(F') \equiv E_0(F)$. If $F \equiv \Pi X^0.F_1$ and $F' \equiv [F''/X^0]F_1$, then $E_0(F) \equiv E_0(F_1)$. By lemma \ref{subeg}, we know $E_0(F') \equiv E_0([F''/X^0]F_1) \equiv [F_2/X^0]E_0(F_1)$ for some $F_2$. 

\end{proof}

\begin{lemma}
  \label{setsub}
  If $F \twoheadrightarrow_{is, gs} F'$, then there exist a substitution $\delta$ with domain
  of set variables and codomain of sets such that $\delta E_1(F) \equiv E_1(F')$.
\end{lemma}
\begin{proof}
    It suffices to consider $ F {\to_{is,gs}} F'$.
If $F' \equiv \Pi X^1 .F$, then $E_1(F') \equiv E_1(F)$.
If $F \equiv \Pi X^1 .F_1$ and $F' \equiv [S/X^1]F_1$, then $E_1(F) \equiv E_1(F_1)$. By lemma \ref{subeg}, we know $E_1(F') \equiv E_1([S/X^1]F_1) \equiv [S/X^1]E_1(F_1)$. 
\end{proof}

\begin{theorem}[Compatibility]
  \label{comp}
  If $(F_1 \to F_2) \to_{\iota,\beta,i,g,I,G, is, gs}^*(F_1' \to F_2')$, then there exists a mixed substitution\footnote{A substitution that contains term, set and formula substitution} $\delta$ such that $ \delta(F_1 \to F_2) \to_{\beta} F_1' \to F_2'$. Thus $\delta F_1 \to_{\beta} F_1'$ and $ \delta F_2 \to_{\beta} F_2'$. 
\end{theorem}

\begin{proof}
  By lemma \ref{termsub}, lemma \ref{formsub} and lemma \ref{setsub}, we have $\delta(F_1 \to F_2) \to_{\beta, \iota} F_1' \to F_2'$ for some mix substitution $\delta$. Since $\to_{\iota}$ reduction can not happen in the sequence $\delta(F_1 \to F_2) \to_{\beta, \iota} F_1' \to F_2'$, so we have $\delta(F_1 \to F_2) \to_{\beta} F_1' \to F_2'$. Thus $\delta F_1 \to_{\beta} F_1'$ and $ \delta F_2 \to_{\beta} F_2'$. 

\end{proof}

\begin{lemma}[Inversion]
  
  \
  
  \begin{itemize}
  \item If $\Gamma \vdash a:F$, then exist $F_1$ such that $F_1 {\to_{\iota,\beta,i,g,I,G, is,gs}^*} F$ and $(x:F_1) \in \Gamma$.

  \item If $\Gamma \vdash p_1 p_2:F$, then exist $F_1, F_2$ such that $\Gamma \vdash p_1:F_1 \to F_2$ and $\Gamma \vdash p_2:F_1$ and $F_2 {\to_{\iota,\beta,i,g,I,G, is, gs}^*} F$. 

\item If $\Gamma \vdash \lambda a.p:F$, then exist $F_1, F_2$ such that $\Gamma, a:F_1 \vdash p:F_2$ and $F_1 \to F_2 {\to_{\iota,\beta,i,g,I,G, is, gs}^*}F$. 

  \end{itemize}
\end{lemma}

\begin{lemma}[Substitution]
\label{subst1}
\

  \begin{enumerate}
  \item   If $\Gamma \vdash p:F$, then for any mixed substitution $\delta$, $\delta \Gamma \vdash p: \delta F$.
\item If $\Gamma, a:F \vdash p:F'$ and $\Gamma \vdash p':F$, then $\Gamma \vdash [p'/a]p:F'$.
  \end{enumerate}

\end{lemma}

\begin{theorem}[Preservation]
  \label{preservation}
If $\Gamma \vdash p : F$ and $p \to_{\beta} p'$, then $\Gamma \vdash p':F$.
\end{theorem}

\begin{proof}
  We list one interesting case:

\

\infer{\Gamma \vdash p_1 p_2:F_2}{\Gamma
\vdash p_1: F_1 \to F_2 & \Gamma \vdash p_2: F_1}

\

\noindent Suppose $\Gamma \vdash (\lambda a.p_1) p_2 \to_{\beta} [p_2/a]p_1$. We know that
$\Gamma \vdash \lambda a.p_1 : F_1 \to F_2$ and $\Gamma \vdash p_2:F_1$. By
inversion on $\Gamma \vdash \lambda a.p_1 : F_1 \to F_2$, we know that 
there exist $F_1', F_2'$ such that $\Gamma, a:F_1' \vdash p_1:F_2'$
and $(F_1' \to F_2') {\to_{\iota,\beta,i,g,I,G, is,gs}^*} (F_1 \to F_2)$. 
By theorem \ref{comp}, we have $ \delta(F_1' \to F_2') =_{\beta} (F_1 \to F_2)$. By Church-Rosser
of $=_{\beta}$, we have $ \delta F_1'=_{\beta}  F_1$ and $\delta F_2' =_{\beta} F_2$. 
So by (1) of lemma \ref{subst1}, we have $\Gamma, a:\delta F_1' \vdash p_1: \delta F_2'$. So $\Gamma, a: \delta F_1' \vdash p_1: F_2$. Since $\Gamma \vdash p_2:\delta F_1'$, by (2) of lemma \ref{subst1}, $\Gamma \vdash [p_2/a]p_1: F_2$. 

\end{proof}


\section{The Polymorphic Dependent Type System $\systemg \lbrack t \rbrack$}
\label{internal}
In this section, we first show a polymorphic dependent type system $\systemg \lbrack t \rbrack$. Then, we define an embedding from $\systemg \lbrack t \rbrack$ to $\systemg$. The embedding is invertable, thus we can transform a judgement in $\systemg$ to a judgement in $\systemg \lbrack t \rbrack$ and vice versa. We call this behavior \textit{reciprocity}. 

\begin{definition}[Syntax]
\

\noindent Lambda Terms $t\ := \ x \ | \ \lambda x.t \ | \ t t'$
 
\noindent Internal Types $U\ := X^1 \ | \ \iota x.Q \ | \ \Pi x:U.U' \ | \ \Delta X^1.U$

\noindent Internal Formula $Q \ := X^0 \ | \ t \ep U \ | \ \Pi X^0.Q \ | \ Q \to Q' \ | \ \forall x.Q \ | \  \Pi X^1. Q$

\noindent Internal Context $\Psi\ :=  \ \cdot \ | \ \Psi, x\ep U$

\end{definition}

Besides basic set formed by formula and set variable, internal types includes dependent-type-like construct $\Pi x:U.U'$ and polymorphic-type-like construct $\Delta X^1.U$. The internal formula stay the same as formula in $\systemg$ except replacing the notion of set by the notion of internal type. We can view $\ep$ relation as a kind of typing relation, thus we have the notion of
internal context as a list of formula of the form $x\ep U$ and the following internal typing relation. 

\begin{definition}[Internal Typing]
  \
  
  \
  
    \begin{tabular}{ll}
%%\infer[toSet]{\intern{\Gamma} \Vdash t': t \ep \intern{S}}{\Gamma \vdash t':t\ep S}

\infer{\Psi \Vdash x \ep U}{x \ep U \in \Psi }

&

\infer{\Psi \Vdash \lambda x.t\ep \Pi x:U. U'}
{\Psi, x \ep U \Vdash  t \ep U'}

\\
\\

\infer{\Psi \Vdash t\ep \Delta X^1. U}
{\Psi \Vdash t\ep U & X^1 \notin FV(\Psi)}

&
\infer{\Psi \Vdash  t\ep [U'/X] U}
{\Psi \Vdash t \ep \Delta X^1.U}

\\
\\
\infer{\Psi \Vdash  t_1 t_2 \ep [t_2/x]U}{\Psi
\Vdash  t_1 \ep \Pi x: U'.U & \Psi \Vdash  t_2 \ep U'}
\end{tabular}
  
\end{definition}

The internal typing shares a lot of similarities between the usual polymorphic dependent type
system. But we want to emphasis that the meaning of internal typing in $\systemg \lbrack t \rbrack$ is different from the usual notion of typing. The internal typing relation is an internal formula in $\systemg \lbrack t \rbrack$ (which lies in the object language), while the ususal notion of typing is a meta-level relation. The emergence of internal typing benefits from the $(\ep, \iota)$-notation. 

Now let us relate $\systemg \lbrack t \rbrack$ with $\systemg$. 

\begin{definition}
    $\interp{\cdot}$ is an \textbf{embedding} from internal types in $\systemg \lbrack t \rbrack$ to sets in $\systemg$, internal formulas in $\systemg \lbrack t \rbrack$ to formulas in $\systemg$.

\noindent  $\interp{X^1} := X^1$

\noindent  $\interp{\iota x.Q} := \iota x.\interp{Q}$

\noindent $\interp{\Pi x:U'.U} := \iota f. \forall x. (x \ep \interp{U'} \to f\ x \ep \interp{U})$, where $f$ is fresh.

\noindent $\interp{\Delta X^1.U} := \iota x. (\Pi X^1. x \ep \interp{U})$, where $x$ is fresh.

\noindent  $\interp{X^0} := X^0$

\noindent  $\interp{t\ep U} := t \ep \interp{U}$

\noindent  $\interp{Q \to Q'} := \interp{Q} \to \interp{Q}$

\noindent  $\interp{\Pi X^i.Q} := \Pi X^i.\interp{Q}$.

\noindent  $\interp{\forall x.Q} := \forall x.\interp{Q}$.

\noindent  $\interp{x\ep U, \Psi} :=  x \ep \interp{U}, \interp{\Psi}$

\end{definition}


\begin{lemma}
\label{subterm}
$[t'/x]\interp{U} = \interp{[t'/x]U}$ and $[\interp{U'}/X^1] \interp{U} = \interp{[U'/X^1]U}$.
\end{lemma}
\begin{proof}
  By induction on structure of $U$.
\end{proof}

\begin{theorem}
 \label{ext}
 If $\Psi \Vdash t \ep U$, then $\interp{\Psi} \vdash  t\ep \interp{U}$.
\end{theorem}
\begin{proof}
  By induction on the derivation of $\Psi \Vdash t \ep U$. 
  
  \noindent \textbf{Case}:

  \
  
\infer{\Psi \Vdash x \ep U}{x\ep U \in \Psi }

\noindent $\interp{\Psi} \vdash x \ep \interp{U}$, since $x\ep \interp{U} \in \interp{\Psi}$.

\noindent \textbf{Case}:

\

\infer{\Psi \Vdash \lambda x.t \ep \Pi x:U. U'}
{\Psi, x\ep U \Vdash t \ep U'}

\noindent By induction, we have $\interp{\Psi}, x\ep \interp{U} \vdash  t \ep \interp{U'}$.
So $\interp{\Psi} \vdash x\ep \interp{U} \to t \ep \interp{U'}$, then by $\forall$-intro
rule, we have $\interp{\Psi} \vdash \forall x.(x\ep \interp{U} \to t \ep \interp{U'})$. By comprehension rule and beta-reduction, we get $\interp{\Psi} \vdash \lambda x.t \ep \iota f.\forall x.(x\ep \interp{U} \to f \ x \ep \interp{U'})$. We know that $\interp{\Pi x:U.U'} := \iota f. \forall x. (x \ep \interp{U} \to f\ x \ep \interp{U'})$. 

\noindent \textbf{Case}:

\

\infer{\Psi \Vdash t t' \ep [t'/x]U}{\Psi
\Vdash t \ep  \Pi x: U'.U & \Psi \Vdash t'\ep U'}

\noindent By induction, we have $\interp{\Psi} \vdash t \ep \iota f. \forall x. (x \ep \interp{U'} \to f\ x \ep \interp{U})$ and $ \interp{\Psi} \vdash t'\ep \interp{U'}$. By comprehension, we have $\interp{\Psi} \vdash \forall x. (x \ep \interp{U'} \to t\ x \ep \interp{U})$. Instantiate $x$ with $t'$, we have $\interp{\Psi} \vdash  t' \ep \interp{U'} \to t\ t' \ep [t'/x] \interp{U}$. So by modus ponens, we have $\interp{\Psi} \vdash t t' \ep [t'/x]\interp{U}$. By lemma \ref{subterm}, we know that $[t'/x]\interp{U} = \interp{[t'/x]U}$. So $\interp{\Psi} \vdash t t' \ep \interp{[t'/x]U}$.

\noindent \textbf{Case}:

\

\infer{\Psi \Vdash t \ep \Delta X^1. U}
{\Psi \Vdash t \ep U & X^1 \notin FV(\Psi)}

\noindent By induction, one has $\interp{\Psi} \vdash  t \ep \interp{U}$. So one has 
$\interp{\Psi} \vdash \Pi X^1. t \ep \interp{U}$. So by comprehension, one has $\interp{\Psi} \vdash t\ep \iota x. \Pi X^1. x \ep \interp{U}$. 

\noindent \textbf{Case}:

\

\infer{\Psi \Vdash t \ep [U'/X] U}
{\Psi \Vdash t \ep \Delta X^1.U}

\noindent By induction, one has $\interp{\Psi} \vdash t \ep \iota x. \Pi X^1. x \ep \interp{U}$. By comprehension, we have $\interp{\Psi} \vdash \Pi X^1. t \ep \interp{U}$. So by instantiation, we have $\interp{\Psi} \vdash t \ep [\interp{U'}/X^1] \interp{U}$. Since by lemma \ref{subterm}, we know $[\interp{U'}/X^1] \interp{U} = \interp{[U'/X^1]U}$.

\end{proof}

We now define the inverse of $\interp{\cdot}$. 

\begin{definition}

\

\noindent $\intern{\cdot}$ is a maping from the sets in $\systemg$ to the internal types in $\systemg \lbrack t \rbrack$, from the formulas in $\systemg$ to the internal formulas $\systemg \lbrack t \rbrack$.

\noindent $\intern{X^1} := X^1$

\noindent $\intern{\iota f. \forall x. (x \ep S' \to f\ x \ep S)} := \Pi x:\intern{S'}.\intern{S}$, where $f$ is fresh.

\noindent $\intern{\iota x. (\Pi X^1. x \ep S)} := \Delta X^1.\intern{S}$, where $x$ is fresh.

\noindent $\intern{\iota x.T} := \iota x.\intern{T}$

\noindent $\intern{X^0} := X^0$

\noindent $\intern{t\ep S} := t \ep \intern{S}$

\noindent $\intern{T \to T'} := \intern{T} \to \intern{T}$

\noindent $\intern{\Pi X^i.T} := \Pi X^i.\intern{T}$.

\noindent $\intern{\forall x.T} := \forall x.\intern{T}$.

\noindent $\intern{x\ep S, \Gamma} := x\ep \intern{S}, \intern{\Gamma}$
\end{definition}

\begin{lemma}
\label{id}
  $\interp{\intern{S}} = S$ and $\intern{\interp{U}} = U$.
\end{lemma}

\begin{proof}
By induction. 
\end{proof}

By lemma \ref{id}, if we have $\Gamma \vdash t \ep S$ in $\systemg$, 
we can go to $\systemg \lbrack t \rbrack$ by $\intern{\Gamma} \Vdash t \ep \intern{S}$. Then, 
after a few deductions in $\systemg \lbrack t \rbrack$, we can use theorem \ref{ext} to go 
back to $\systemg$. 

\section{Proving Peano's Axioms}
\label{peano}
In this section, we show how to prove all of Peano's axioms in $\systemg$. First, let us
see the definition of natural number.

\begin{definition}[Scott Numerals]
  \
  
  \noindent $\mathsf{Nat} := \iota x. \Pi C^1.(\forall y . ( (y \ep C) \to (\mathsf{S} y) \ep C)) \to 0 \ep C  \to x \ep C$

\noindent $\mathsf{S} \ := \lambda n. \lambda s.\lambda z. s \ n$

\noindent $0\  := \lambda s. \lambda z.z$

\end{definition}

We define the set of numerals $\nat$, and the $\suc, 0$ are Scott encoded numerals. 

\begin{theorem}[Peano's Axiom 1]
  $\vdash 0 \ep \nat$.
\end{theorem}
\begin{proof}
By comprehension, we want to show $\vdash \Pi C^1.(\forall y . ( (y \ep C) \to (\mathsf{S} y) \ep C)) \to 0 \ep C  \to 0 \ep C$, which is obvious\footnote{Note the proof terms for the theorem is Church numeral $0$.}. 
\end{proof}

\begin{definition}[Leibniz Equality]
  $x = y\ := \ \Pi C^1. x \ep C \to y \ep C$.
\end{definition}
\begin{theorem}[Peano Axiom 2-4]
\

\begin{enumerate}
  \item $\forall x. x = x $.
  \item $\forall x.\forall y . x = y \to y = x$.
  \item $\forall x.\forall y. \forall z. x = y \to y = z \to x = z$.
  \end{enumerate}
\end{theorem}
\begin{proof}
  We only prove 2, the others are easy. Assume $\Pi C^1. x\ep C \to y \ep C$(1), we want to show $ y \ep A \to x \ep A$ for any $A^1$. Instantiate $C$ in (1) with $\iota z.  (z \ep A \to x \ep A)$. By comprehension, we get $(x \ep A \to x \ep A) \to (y \ep A \to x \ep A)$. And we know that $x \ep A \to x \ep A$ is derivable in our system, so by modus ponens we get $y \ep A \to x \ep A$. 
\end{proof}

\begin{lemma}
\label{oconv}
   $\cdot \vdash \forall a. \forall b. \Pi P^1. ( a \ep P \to a = b \to b \ep P)$. 
\end{lemma}
\begin{proof}
  By modus ponens.
\end{proof}
\begin{theorem}[Peano's Axiom 5]
   $\cdot \vdash  \forall a. \forall b. (a \ep \mathsf{Nat} \to a = b \to b \ep \mathsf{Nat})$.
\end{theorem}
\begin{proof}
  Let $P := \iota x.x\ep \mathsf{Nat}$ for lemma \ref{oconv}. 
\end{proof}


\begin{theorem}[Peano's Axiom 6]
  \label{succ}
$\cdot \vdash \forall m. (m \ep \mathsf{Nat} \to \mathsf{S}m \ep \mathsf{Nat})$.
\end{theorem}
\begin{proof}
Assume $m \ep \mathsf{Nat}$. We want to show $\mathsf{S}m \ep \mathsf{Nat}$. By comprehension, we just need to show $ \Pi C^1.(\forall y . ( (y \ep C) \to (\mathsf{S} y) \ep C)) \to 0 \ep C  \to \suc m \ep C$. By Intros, we want to derive $m \ep \mathsf{Nat}, \forall y . ( (y \ep C) \to (\mathsf{S} y) \ep C), 0 \ep C \vdash \suc m \ep C$. Since $m \ep \mathsf{Nat}$, we know that $\Pi C^1.(\forall y . ( (y \ep C) \to (\mathsf{S} y) \ep C)) \to 0 \ep C  \to m \ep C$. By Modus Ponens, we have $ m \ep C$. We know that $m \ep \mathsf{Nat}, \forall y . ( (y \ep C) \to (\mathsf{S} y) \ep C), 0 \ep C \vdash (m \ep C) \to (\mathsf{S} m)\ep C$. Thus we derive $m \ep \mathsf{Nat}, \forall y . ( (y \ep C) \to (\mathsf{S} y) \ep C), 0 \ep C \vdash \suc m \ep C$, which is what we want\footnote{Note that the proof term for this theorem is Church successor.}. 
  \end{proof}

\begin{theorem}[Induction Principle]
  \label{induction}
\

\noindent  $\vdash \Pi C^1. (\forall y . ( (y \ep C) \to (\mathsf{S} y) \ep C)) \to 0 \ep C \to \forall m. (m \ep \mathsf{Nat} \to m \ep C)$

\end{theorem}
\begin{proof}
Assume $\forall y . ( (y \ep C) \to (\mathsf{S} y) \ep C), 0 \ep C$ and $m \ep \mathsf{Nat}$. We need to show that $m \ep C$. Since $m \ep \mathsf{Nat}$ implies that $\Pi C^1.(\forall y . ( (y \ep C) \to (\mathsf{S} y) \ep C)) \to 0 \ep C  \to m \ep C$. So by instantiation and modus ponens we get $m \ep C$. \footnote{The proof terms for this theorem is $\lambda s. \lambda z. \lambda n. n\ s\ z$.}

\end{proof}

In order to proceed to prove Peano's axiom 7, we need to define a notion of contradiction in $\systemg$. 

\begin{definition}[Notion of Contradiction]
  $\bot := \forall x. \forall y. (x = y)$.  
\end{definition}

\begin{theorem}[Consistency (Meta)\footnote{Meaning the proof of this theorem relies on meta-level argument.}]
  \label{contradiction}
  $\bot$ is uninhabited in $\systemg \lbrack p \rbrack$.
\end{theorem}
\begin{proof}
  Suppose $\bot$ is inhabited, that is, there is a proof term $p$ such that 
  $\cdot \vdash p : \forall x. \forall y. \Pi C^1. x \ep C \to y\ep C$. By theorem \ref{const} and theorem \ref{preservation}, we know that $p$ must normalized at some normal proof term $p'$
  such that $\cdot \vdash p' : \forall x. \forall y. \Pi C^1. x \ep C \to y\ep C$. We know that $p'$ must of the form $\lambda a.p''$ with $a: x \ep C$. Since $=_{\beta, \iota}$ is Church-Rosser, we can not convert $x\ep C$ to $y \ep C$. So $p'$ can not exist.   
\end{proof}

\begin{lemma}
  \label{zero1}
  $\vdash 0 = \suc 0 \to \bot$.
\end{lemma}
\begin{proof}
Assume $0 = \suc 0$, namely, $\Pi C^1. 0 \ep C \to \suc 0 \ep C$ $\dagger$. We want to show $\forall x.\forall y. \Pi A^1. x \ep A \to y \ep A$. 
Assume $x \ep A$ (1). We now instantiate $C$ with $\iota u. (((\lambda n. n\ (\lambda z.y)\ x)\ u) \ep A)$ in $\dagger$. By comprehension and beta reduction, we get $x \ep A \to y \ep A$ (2). By modus ponens of (1), (2), we get $y \ep A$. 
\end{proof}

We also need predecessor to prove Peano's axiom 7. 
\begin{definition}
  $\pred := \lambda n. n  (\lambda x.x) 0$.
\end{definition}

\begin{lemma}[Congruence of Equality]
  \label{cong}
  $\vdash \forall a.\forall b.\forall f. a = b \to f a = f b$.
\end{lemma}
\begin{proof}
  Assume $\Pi C. a \ep C \to b \ep C$. Let $C := \iota x. f x \ep P$ with $P$ free. Instantiate $C$ for the 
assumption, we get $a \ep (\iota x. f x \ep P) \to b \ep (\iota x. f x \ep P)$. By conversion, 
we get $f\ a \ep P \to f\ b \ep P$. So by polymorphic generalization, we get $f\ a = f\ b$.
  
\end{proof}

\begin{theorem}[Peano's Axiom 7]
  $\vdash \forall n. n \ep \nat \to (\suc n = 0 \to \bot)$
\end{theorem}
\begin{proof}
  We will use induction principle (theorem \ref{induction}) to prove this. We instantiate 
  $C$ in theorem \ref{induction} with $\iota z. (\suc z = 0 \to \bot)$, we have $ \forall y . ( (\suc y = 0 \to \bot ) \to (\suc \mathsf{S} y = 0 \to \bot)) \to (\suc 0 = 0 \to \bot) \to \forall m. (m \ep \mathsf{Nat} \to (\suc m = 0 \to \bot))$. Base case is by lemma \ref{zero1}. For the step case, we assume $\suc y = 0 \to \bot$ (IH), we want to show $\suc \mathsf{S} y = 0 \to \bot$. 
  Assuming $\suc \suc y = 0$, we want to show $\bot$. By lemma \ref{cong}, we know that $\pred(\suc \suc y) = \pred 0$. By beta-reduction, we have $\suc y = 0$. Thus by IH, we have $\bot$. 
\end{proof}


\begin{theorem}[Peano's Axiom 8]
  $\forall m. \forall n. m\ep \nat \to n\ep \nat \to \suc m = \suc n \to m = n$.
\end{theorem}
\begin{proof}
Assume $\suc m = \suc n$. By lemma \ref{cong}, we have $\pred (\suc m) = \pred (\suc n)$. So 
by beta reduction, we have $m = n$.
\end{proof}

In order to state Peano's axiom 9, we need to extend the formula in $\systemg$ with $F \wedge F'$. And the proof of $F\wedge F'$ consist of both the proof of $F$ and the proof of $F'$.

\begin{theorem}[Peano's Axiom 9, Weak Induction]
 \
 
  \noindent  $\vdash \Pi C^1. (\forall y . (y\ep \nat \wedge (y \ep C) \to (\mathsf{S} y) \ep C)) \to 0 \ep C \to \forall m. (m \ep \mathsf{Nat} \to m \ep C)$
\end{theorem}
\begin{proof}
  Assume $\forall y . (y\ep \nat \wedge (y \ep C) \to (\mathsf{S} y) \ep C)$ $\dagger$ and $0 \ep C$. We want to show that $\forall m. (m \ep \mathsf{Nat} \to m \ep C)$. We just need to show $\forall m. (m \ep \mathsf{Nat} \to (m \ep \nat \wedge m \ep C))$. We prove this using theorem \ref{induction}. For the base case, it is obvious that $0 \ep \nat \wedge 0 \ep C$. For step case, assuming $z\ep \nat \wedge z\ep C$ (IH), we need to show $\suc z \ep \nat \wedge \suc z\ep C$. By theorem \ref{succ}, we have $\suc z \ep \nat$. By $\dagger$, we know that $\suc z \ep C$. Thus $\forall z. (z \ep \mathsf{Nat} \to (z \ep \nat \wedge z \ep C))$. 
\end{proof}

We have proved all Peano's nine axioms. We could continue to define $<$ relation for natural
number and prove strong induction principle from the weak induction principle, and go further 
to formalize more mathematics. But we will not do that here.

\section{Reasoning about Programs}
\label{prog}
System $\systemg$ is expressive enough to reason about programs. Here by programs we mean 
pure lambda calculus with Scott encoding. We will show some simple examples about Scott numerals, and then we show how to encode Vector with $\systemg$.

\begin{definition}
  $\mathsf{add} :=  \lambda n. \lambda m.n\ (\lambda p. \mathsf{add}\ p\ (\mathsf{S} m))\ m$
\end{definition}

\noindent We know that the above recursive equation can be solved by fixpoint. But we do not 
bother to solve it. The way we treat it is use it as a kind of build in beta equality, when
every we see a $\mathsf{add}$, we one step unfold it. 

\begin{theorem}
$\cdot \vdash \forall n. (n \ep \mathsf{Nat} \to \mathsf{add}\ n\ 0 = n)$. 
\end{theorem}
\begin{proof}

We want to show $\forall n. (n \ep \mathsf{Nat} \to \mathsf{add}\ n\ 0 = n)$.
 Let $P := \iota x. \mathsf{add}\ x\ 0 = x$. Instantiate the $C^1$ in theorem \ref{induction} with $P$, we get $\forall y . ( \mathsf{add}\ y\ 0 = y \to \mathsf{add}\ (\mathsf{S} y)\ 0 = \mathsf{S} y) \to\mathsf{add}\ 0\ 0 = 0 \to \forall m. (m \ep \mathsf{Nat} \to m \ep P)$. We just have to prove $\forall y . ( \mathsf{add}\ y\ 0 = y \to \mathsf{add}\ (\mathsf{S} y)\ 0 = \mathsf{S} y)$ and $\mathsf{add}\ 0\ 0 = 0$. For the base case, we want to show $\Pi C. \mathsf{add}\ 0\ 0 \ep C \to 0 \ep C$. Assume $\mathsf{add}\ 0\ 0 \ep C$, since $\mathsf{add}\ 0\ 0 \to_{\beta} 0$, by conversion, we get $0 \ep C$. For the step case is a bit complicated, assume $\mathsf{add}\ y\ 0 = y$, we want to show $\mathsf{add}\ (\mathsf{S} y)\ 0 = \mathsf{S} y$. Since $\mathsf{add}\ y\ 0 \to_{\beta} y\ (\lambda p.\mathsf{add}\ p\ (\suc 0))\ 0$,  And $\mathsf{add}\ (\mathsf{S}y)\ 0 \to_{\beta} \mathsf{add} \ y \ (\suc 0) \leftarrow_{\beta}^* \suc (\mathsf{add}\ y\ 0)$. So lemma \ref{cong} will give us this. 
\end{proof}

\begin{theorem}
$\cdot \vdash \forall n. (n \ep \mathsf{Nat} \to \forall m.(m\ep \nat \to \mathsf{add}\ n\ m \ep \nat))$. 
  After transformed to $\systemg \lbrack t \rbrack$, we have $\Vdash \add \ep \nat \to \nat \to \nat$. \footnote{We write $U \to U'$ if $\Pi x:U.U'$ with $x \notin \mathrm{FV}(U')$.}
\end{theorem}
\begin{proof}
  Let $P := \iota z.\forall m.(m\ep \nat \to \mathsf{add}\ z\ m \ep \nat)$. We instantiate the
  $C$ in theorem \ref{induction}, we have $(\forall y . ( (y \ep P) \to (\mathsf{S} y) \ep P)) \to 0 \ep P \to \forall m. (m \ep \mathsf{Nat} \to m \ep P)$. For the base case, we need to show $\forall m.(m\ep \nat \to \mathsf{add}\ 0\ m \ep \nat)$. By $\mathsf{add}\ 0\ m \to_{\beta} m$,
  we have the base case. For the step case, assuming $\forall m.(m\ep \nat \to \mathsf{add}\ y\ m \ep \nat)$ (IH), we need to show $\forall m.(m\ep \nat \to \mathsf{add}\ (\suc y)\ m \ep \nat)$. We know that $\mathsf{add}\ (\suc y)\ m \to_{\beta}^* \add \ y \ (\suc m)$. By (IH), we know
  $\add \ y \ (\suc m) \ep \nat$. So $\mathsf{add}\ (\suc y)\ m \ep \nat$. 
\end{proof}

\subsection{Termination Analysis in System $\systemg$}
In this section, we will show that elements in the inductive defined set are solvable. A direct consequence of this result is that these elements is terminating with respect to head reduction.

\subsubsection{Preliminary}
The definitions, lemmas and theorems in this subsection come from Barendregt's \cite{Barendregt:1985}, Chapter 8.3.

\begin{definition}[Solvability]
\

  \begin{itemize}
  \item   A closed lambda term $t$, i.e. $\mathrm{FV}(t) = \emptyset$, is solvable if
there exists $t_1,..., t_n$ such that $t t_1 ... t_n =_{\beta} \lambda x.x$.
\item An arbitrary term $t$ is solvable if the closure $\lambda x_1...\lambda x_n.t$, where
$\{x_1,...,x_n\} = \mathrm{FV}(t)$, is solvable.
  \item $t$ is unsolvable iff $t$ is not solvable.
  \end{itemize}
\end{definition}

\begin{lemma}
  Every term $t$ is of the following forms:
  \begin{itemize}
  \item $\lambda x_1....\lambda x_n.x t_1...t_m$, where $n,m \geq 0$. It is called head normal form. 
  \item $\lambda x_1....\lambda x_n.((\lambda y.t) t_1)...t_m$, where $(\lambda y.t) t_1$ is called head redex.
  \end{itemize}
\end{lemma}
\begin{definition}[Head Reduction]
  $t \to_h t'$ if $t'$ is resulting from contracting the head redex of $t$. 
\end{definition}
\begin{theorem}
  A term $t$ has a head normal form iff it is terminating with respect to head reduction.
\end{theorem}
\begin{theorem}[Wadsworth]
  $t$ is solvable iff $t$ has a head normal form. In particular, all terms in
normal forms are solvable, and unsolvable terms have no normal form.
\end{theorem}

\begin{theorem}[Genericity]
  \label{general}
  For a unsolvable term $t$, if $t_1 t =_{\beta} t_2$, where $t_2$ in normal form, then
for any $t'$, we have $t_1 t' =_{\beta} t$.
\end{theorem}

So unsolvable in general is computational irrelavance, thus it is reasonable to equate
all unsolvable terms. 

\begin{definition}[Omega-Reduction]
Let $\Omega$ be $(\lambda x.xx)\lambda x.xx$, then $t \to_{\omega} \Omega$ iff $t$ is unsolvable and $t \not \equiv \Omega$.
%  $\lambda x.t x \to_{\eta} t$ if $x \notin \mathrm{FV}(t)$. 

\end{definition}

\begin{theorem}
  $\to_{\beta} \cup \to_{\omega}$ is Church-Rosser.
\end{theorem}

\subsubsection{Head Normalization}
\label{head}
We add Omega-reduction as part of the term reduction in $\mathfrak{G}$. We now define another notion of contradictory: $\bot' := \forall x. x = \Omega$. Note that this will imply $\forall x.\forall y. x = y$, thus we can safely take it as contradictory.

\begin{theorem}
  \label{omega}
  $\vdash \forall n. ( n \ep \mathsf{Nat} \to (n = \Omega \to \bot'))$.
\end{theorem}
\begin{proof}
  We will prove this by induction. Recall the induction principle:  
  
  $\Pi C^1. (\forall y . ( (y \ep C) \to (\mathsf{S} y) \ep C)) \to 0 \ep C \to \forall m. (m \ep \mathsf{Nat} \to m \ep C)$.
  
  \noindent We instantiate $C$ with $\iota z. (z = \Omega \to \bot')$, by comprehension, we then have $(\forall y . ( (y = \Omega \to \bot'  ) \to (\mathsf{S} y = \Omega \to \bot')) \to (0 = \Omega \to \bot') \to \forall m. (m \ep \mathsf{Nat} \to (m = \Omega \to \bot'))$. It is enough to show that $0 = \Omega \to \bot'$ and $\mathsf{S} y = \Omega \to \bot'$. We know that for Scott numerals we have $0 := \lambda s.\lambda z.z$ and $\suc y := \lambda s.\lambda z.s y$. Assume $0 = \Omega = \lambda x_1.\lambda x_2.\Omega$, let $F := \lambda u. u \ p\ q$. Assume $q \ep X^1$, then $F \ 0 \ep X^1$ (since $F0 =_{\beta}q$). So $F \ (\lambda x_1.\lambda x_2.\Omega) \ep X^1$, thus $\Omega \ep X^1$. Thus we just show
$\forall X^1. (q \ep X^1 \to \Omega \ep X^1)$, which means $\forall q. q = \Omega$. So $0 = \Omega \to \bot'$. Now let us show $\mathsf{S} y = \Omega \to \bot'$. Assume $\lambda s.\lambda z.sy = \Omega = \lambda x_1.\lambda x_2.\Omega$. Let $F := \lambda n.n\ (\lambda p.q)\ z$. Assume $q \ep X^1$, then $F\ (\lambda s.\lambda z.s y) \ep X^1$, thus $F\ (\lambda x_1.\lambda x_2.\Omega) \ep X^1$, meaning $\Omega \ep X^1$. So we just show $\Pi X^1. (q \ep X \to \Omega \ep X)$. Thus $\forall q. q = \Omega$. So $\mathsf{S} y = \Omega \to \bot'$.  
\end{proof}

Above theorem implies that all the member of $\mathsf{Nat}$ has a head normal form and it can be generalized to show that the elements of inductive describable set are solvable. To see this, we prove the following meta-theorem.

\begin{theorem}
 If $\vdash t \ep \nat$, then $t \not =_{\beta,\omega} \Omega$.
\end{theorem}
\begin{proof}
By theorem \ref{omega}, we know that $\vdash t = \Omega \to \bot$. We know that by the \textit{conv} rule, if $t =_{\beta, \omega} t'$, then $\vdash t = t'$ in $\systemg$. By contraposition, we have if $\not\vdash t = t'$, then $t \not =_{\beta, \omega} t'$. Since $\systemg$ is consistent (theorem \ref{contradiction}), we know that $\not \vdash t = \Omega$. So $t \not =_{\beta, \omega} \Omega$.
\end{proof}
\subsection{Leibniz Equality in $\mathfrak{G}$}
\label{leibniz}

We know that by the \textit{conv} rule, if $t =_{\beta,\eta, \omega} t'$, then $\vdash t = t'$ in $\systemg$. It is natural to consider wether the other direction is the case, namely, to prove: if $\vdash t = t'$, then $t=_{\beta, \eta, \omega} t'$. By the contraposition, we have: if $t\not =_{\beta, \eta, \omega} t'$, then  $\not\vdash t = t'$. We conjecture that it is hard to prove this. Due to the genericity (theorem \ref{general}) property in lambda calculus. Oraclely, if $t$ is solvable and $t'$ is unsolvable, we can not define a lambda term $F$ such that $F t =_{\beta} x$ and $F t' =_{\beta} y$. Because by genericity, we would have $F t =_{\beta} y$, thus $x =_{\beta}y$, which is impossible for beta-reduction. However, when $t,t'$ both are solvable and $t \not =_{\beta,\eta} t'$, then by the results of Coppo et al. \cite{Coppo:1978}, we can indeed define a lambda term $F$ such that $F t =_{\beta} x$ and $F t' =_{\beta} y$. So we can derive $\vdash t = t' \to \bot$ in System $\systemg$. 

%% \begin{theorem}\footnote{This theorem comes from Barendregt's \cite{Barendregt:1985}, page 396.} 
%%   \label{sep}
%%   Let $t_1, t_2$ be two closed beta-eta normal forms, then there exists a closed term 
%%   $F$ such that:
  
%%   $F t_1 t_2 =_{\beta} \mathsf{True} \equiv \lambda x.\lambda y.x$ if $t_1 \equiv t_2$. 
  
%%   $F t_1 t_2 =_{\beta} \mathsf{False} \equiv \lambda x.\lambda y.y$ if $t_1 \not \equiv t_2$. 
  
%% \end{theorem}



%% \begin{theorem}
%%   \label{neg}
%%   If $t_1$ and $t_2$ are distinct beta-eta normal forms, then $\vdash (t_1 = t_2) \to \bot$.
%% \end{theorem}
%% \begin{proof}
%%   Assume $t_1 = t_2$. By theorem \ref{sep}, we know that $F t_1 t_1 = \mathsf{True}$. Thus 
%%   we have $F t_1 t_2 = \mathsf{True} = \mathsf{False}$. This will lead to a contradiction.
%% \end{proof}

\begin{theorem}
  Assume $t_1, t_2$ are solvable terms. If $\vdash t_1 = t_2$ in $\mathfrak{G}$, then $t_1 =_{\beta\eta} t_2$. 
\end{theorem}
\begin{proof}
 By contraposition, we want to prove: if $t_1 \not =_{\beta\eta} t_2$, then $\not \vdash t_1 = t_2$. Since $t_1$ and $t_2$ are \textit{distinct}, then $t_1$ and $t_2$ are \textit{separable}\footnote{See Barendregt's \cite{Barendregt:1985}, Page 256}. i.e. there exists a lambda term $F$ such that $F t_1 =_{\beta} x$ and $F t_2 =_{\beta} y$. Thus we can derive $\vdash t = t' \to \bot$. Since $\mathfrak{G}$ is consistent, we have $\not \vdash t_1 = t_2$.
\end{proof}

%% When we think about Leibniz law of identity in generals, it is also strongest version of 
%% equality, namely, identity. So intuitively, Leibniz equality in $\mathfrak{G}$ should be corresponded to a notion of intensional identity. And the conversion rule allows us to treat $\beta\eta\Omega$ equivalence as the intensional identity in $\mathfrak{G}$. 
The developments in this section together with section \ref{head} shows that if $\vdash t = t' \to \bot$ in $\systemg$, then $t\not=_{\beta,\eta,\omega} t'$. And if $t_1, t_2$ are solvable terms, then $\vdash t_1 = t_2$ in $\mathfrak{G}$ implies $t_1 =_{\beta\eta} t_2$. 


\subsection{Vector Encoding in System $\systemg$}

In order to do vector encoding in $\systemg$, we need to extend the formulas of $\systemg$
to specify binary relation, so we add the following syntatic category.

\begin{definition}[Relation]
  \
  
\noindent  Formula $F \ ::= ... \ | \ (t;t') \ep R \ | \ \Pi X^2. F$

\noindent  Binary Relation $R \ :: = X^2 \ | \ \iota(x;y).F$

\noindent Relational Comprehension $(t;t') \ep \iota(x;y).F =_{\iota} [(t;t')/(x;y)]F$
\end{definition}

\begin{definition}[Vector]
\

\noindent  $\mathsf{vec}(U, n) := $

$\iota x. \Pi C^2. (\forall y. \forall m. \forall u. (m\ep \mathsf{Nat} \to u \ep U \to (y;m) \ep C  \to (\mathsf{cons}\ m\ u\ y; \mathsf{S}m) \ep C )) \to (\mathsf{nil}; 0) \ep C \to (x; n) \ep C$

\noindent $\nil := \lambda y. \lambda x.x$

\noindent $\cons := \lambda n.\lambda v. \lambda l. \lambda y. \lambda x.y \ n\ v\ l$.

\end{definition}
\begin{lemma}
  $\vdash \nil \ep \vecc(U, 0)$.
\end{lemma}

\begin{lemma}
  \label{veccons}
  $\vdash \forall n. n\ep \mathsf{Nat} \to \forall u. (u \ep U \to \forall l . (l \ep \vecc (U, n) \to (\cons\ n\ u\ l) \ep \vecc (U, \suc n)))$.
  Transform to $\systemg \lbrack t \rbrack$, we get $\Vdash \cons \ep \Pi n: \mathsf{Nat}.U \to \vecc (U, n) \to \vecc (U, \suc n)$. 
    
\end{lemma}
\begin{proof}
Assume $n\ep \mathsf{Nat}, u\ep U, l\ep \vecc (U, n)$. We want to show $(\cons\ n\ u\ l) \ep \vecc (U, \suc n)$. By comprehension, we need to show $\Pi C^2. (\forall y. \forall m. \forall u. (m\ep \mathsf{Nat} \to u \ep U \to (y;m) \ep C  \to (\mathsf{cons}\ m\ u\ y; \mathsf{S}m) \ep C )) \to (\mathsf{nil}; 0) \ep C \to ((\cons\ n\ u\ l); \suc n) \ep C$. Assume that we have $\forall y. \forall m. \forall u. (m\ep \mathsf{Nat} \to u \ep U \to (y;m) \ep C  \to (\mathsf{cons}\ m\ u\ y; \mathsf{S}m) \ep C )$ $\dagger$ and $(\mathsf{nil}; 0) \ep C$, we need to show that $((\cons\ n\ u\ l);\suc n) \ep C$. We know that $l\ep \vecc (U, n)$, by comprehension, we have 

$\Pi C^2. (\forall y. \forall m. \forall u. (m\ep \mathsf{Nat} \to u \ep U \to (y;m) \ep C  \to (\mathsf{cons}\ m\ u\ y; \mathsf{S}m) \ep C )) \to (\mathsf{nil}; 0) \ep C \to (l; n) \ep C$. 

\noindent By modus ponens, we have $(l; n) \ep C$. Instantiate $y$ with $l$, $m$ with $n$, $u$ with $u$ in $\dagger$, we have $n\ep \mathsf{Nat} \to u \ep U \to (l;n) \ep C  \to (\mathsf{cons}\ n\ u\ l; \mathsf{S}n) \ep C $. So by modus ponens, we have $(\mathsf{cons}\ n\ u\ l; \mathsf{S}n) \ep C$.
  
\end{proof}

\begin{theorem}[Induction Principle]
  \label{indvec}
\

\noindent  $\vdash \mathsf{Ind}(U, n) := $

$\Pi C^2. (\forall y. \forall m. \forall u. (m\ep \mathsf{Nat} \to u \ep U \to (y;m) \ep C  \to (\mathsf{cons}\ m\ u\ y; \mathsf{S}m) \ep C )) \to (\mathsf{nil}; 0) \ep C \to \forall l.( l\ep \vecc(U,n) \to (l; n) \ep C)$
\end{theorem}
\begin{proof}
  \noindent Assume we have $ l\ep \vecc(U,n)$ and
  
  $\forall y. \forall m. \forall u. (m\ep \mathsf{Nat} \to u \ep U \to (y;m) \ep C  \to (\mathsf{cons}\ m\ u\ y; \mathsf{S}m) \ep C ), (\mathsf{nil}; 0) \ep C$.
  
  \noindent We want to show $(l; n) \ep C$. By comprehension, we have
  
 $\Pi C^2. (\forall y. \forall m. \forall u. (m\ep \mathsf{Nat} \to u \ep U \to (y;m) \ep C  \to (\mathsf{cons}\ m\ u\ y; \mathsf{S}m) \ep C )) \to (\mathsf{nil}; 0) \ep C \to (l; n) \ep C$. 
  
  \noindent By modus ponens, we have $(l; n) \ep C$.

\end{proof}

\begin{definition}[Append]
\

\noindent  $\app := \lambda n_1. \lambda n_2.\lambda l_1.\lambda l_2. l_1 (\lambda m. \lambda h. \lambda t. \cons\ (m+n_2) \ h \ (\app \ m \ n_2\ t\ l_2)) l_2$ 

\end{definition}

\begin{theorem}
  $\Vdash \app \ep \Pi n_1:\mathsf{Nat}. \Pi n_2:\mathsf{Nat}. \vecc(U, n_1) \to \vecc(U, n_2) \to \vecc(U, n_1+n_2)$
\end{theorem}
\begin{proof}
  Note that we state the theorem in $\systemg \lbrack t \rbrack$. So we want to derive
  
 $n_1 \ep \nat, n_2 \ep \nat \Vdash \lambda l_1. \lambda l_2. l_1 (\lambda m. \lambda h. \lambda t. \cons\ (m+n_2) \ h \ (\app \ m \ n_2\ t\ l_2)) l_2\  \ep $
  
\noindent $\vecc(U, n_1) \to \vecc(U, n_2) \to \vecc(U, n_1+n_2)$. 
  
\noindent  We now transform it back to $\systemg$, we have: 

\noindent $n_1 \ep \nat, n_2 \ep \nat \vdash \forall x_1. x_1 \ep \vecc(U, n_1) \to$

\noindent $ \forall x_2. (x_2 \ep \vecc(U, n_2) \to  x_1 (\lambda m. \lambda h. \lambda t. \cons\ (m+n_2) \ h \ (\app \ m \ n_2\ t\ x_2)) x_2 \ep \vecc(U, n_1+n_2))$. 

\noindent We instantiate the $C$ in theorem \ref{indvec} by

\noindent $P := \iota \gray{$(l;n)$}.\forall x_2. (x_2 \ep \vecc(U, n_2) \to $

\noindent $\gray{$l$} (\lambda m'. \lambda h. \lambda t. \cons\ (m'+n_2) \ h \ (\app \ m' \ n_2\ t\ x_2)) x_2 \ep\vecc(U, \gray{$n$}+n_2))$. 

\noindent So we get 

$(\forall y. \forall m. \forall u. (m\ep \mathsf{Nat} \to u \ep U \to (y;m) \ep P  \to (\mathsf{cons}\ m\ u\ y; \mathsf{S}m) \ep P )) \to (\mathsf{nil}; 0) \ep P \to \forall l.( l\ep \vecc(U,n) \to (l; n) \ep P)$.

%% \noindent $(\forall y. \forall m. \forall u. (m\ep \mathsf{Nat} \to u \ep U \to $

%% \noindent $(\forall x_2. (x_2 \ep \vecc(U, n_2) \to  y (\lambda m'. \lambda h. \lambda t. \cons\ (m'+n_2) \ h \ (\app \ m' \ n_2\ t\ x_2)) x_2 \ep \vecc(U, m+n_2))) \to $

%% \noindent $(\forall x_2. (x_2 \ep \vecc(U, n_2) \to (\cons\ m\ u\ y) (\lambda m'. \lambda h. \lambda t. \cons\ (m'+n_2) \ h \ (\app \ m' \ n_2\ t\ x_2)) x_2 \ep \vecc(U, \mathsf{S}m+n_2)))$

%% \noindent $\to (\forall x_2. (x_2 \ep \vecc(U, n_2) \to (\nil (\lambda m'. \lambda h. \lambda t. \cons\ (m'+n_2) \ h \ (\app \ m' \ n_2\ t\ x_2)) x_2 \ep \vecc(U, 0+n_2)))) \to $

%% \noindent $(\forall x_1. x_1 \ep \vecc(U, n_1) \to \forall x_2. (x_2 \ep \vecc(U, n_2) \to $

%% \noindent $ x_1 (\lambda m. \lambda h. \lambda t. \cons\ (m+n_2) \ h \ (\app \ m \ n_2\ t\ x_2)) x_2 \ep \vecc(U, n_1+n_2)))$. 

\noindent For the base case, we can easily prove 

$\forall x_2. (x_2 \ep \vecc(U, n_2) \to (\nil (\lambda m'. \lambda h. \lambda t. \cons\ (m'+n_2) \ h \ (\app \ m' \ n_2\ t\ x_2)) x_2 \ep \vecc(U, 0+n_2)))$. 

\noindent For the step case, assume (IH)

\noindent $\forall x_2. (x_2 \ep \vecc(U, n_2) \to  y (\lambda m'. \lambda h. \lambda t. \cons\ (m'+n_2) \ h \ (\app \ m' \ n_2\ t\ x_2)) x_2 \ep \vecc(U, m+n_2))$, 

\noindent we want to show that

$\forall x_2. (x_2 \ep \vecc(U, n_2) \to (\cons\ m\ u\ y) (\lambda m'. \lambda h. \lambda t. \cons\ (m'+n_2) \ h \ (\app \ m' \ n_2\ t\ x_2)) x_2 \ep \vecc(U, \mathsf{S}m+n_2))$. 

\noindent We know that 

\noindent $(\cons\ m\ u\ y) (\lambda m'. \lambda h. \lambda t. \cons\ (m'+n_2) \ h \ (\app \ m' \ n_2\ t\ x_2)) x_2 \to_{\beta}^* $

\noindent $\cons (m+n_2)\ u\ (\app\ m \ n_2 \ y\ x_2)\to_{\beta}^*$

\noindent $\cons\ (m+n_2)\ u\ (y \ (\lambda m'.\lambda h.\lambda t.\cons (m'+n_2)\ h \ (\app \ m'\ n_2 \ t\ x_2))x_2))$. 

\noindent By (IH), we know that

\noindent $y (\lambda m'. \lambda h. \lambda t. \cons\ (m'+n_2) \ h \ (\app \ m' \ n_2\ t\ x_2)) x_2 \ep \vecc(U, m+n_2)$. 

\noindent By lemma \ref{veccons} $\cons\ (m+n_2)\ u\ (y \ (\lambda m'.\lambda h.\lambda t.\cons (m'+n_2)\ h \ (\app \ m'\ n_2 \ t\ x_2))x_2)) \ep \vecc(U, \suc(m+n_2))$. Thus 
$(\cons\ m\ u\ y) (\lambda m'. \lambda h. \lambda t. \cons\ (m'+n_2) \ h \ (\app \ m' \ n_2\ t\ x_2)) x_2 \ep \vecc(U, \suc(m+n_2))$. Of course, we assume we have $\suc(m+n_2) = \suc m + n_2$, so we have the proof.

\end{proof}

\begin{theorem}[Associativity]
  
  $ \vdash \forall (n_1. n_2. n_3. v_1. v_2.v_3).(n_1 \ep \mathsf{Nat} \to n_2 \ep \mathsf{Nat} \to n_3 \ep \mathsf{Nat} \to v_1 \ep \vecc(U, n_1) \to v_2 \ep \vecc(U, n_2)) \to v_3 \ep \vecc(U, n_3) \to $
  
  \noindent $\app \ n_1\ (n_2+n_3)\ v_1 \ (\app\ n_2\ n_3 \ v_2 \ v_3) = \app \ (n_1 + n_2) \ n_3\ (\app \ n_1 \ n_2 \ v_1 \ v_2) \ v_3$
\end{theorem}

\begin{proof}
  Assume $n_1 \ep \mathsf{Nat}, n_2 \ep \mathsf{Nat}, n_3 \ep \mathsf{Nat}, v_2 \ep \vecc(U, n_2)) , v_3 \ep \vecc(U, n_3)$. We want to show 
  
  $\forall v_1. (v_1 \ep \vecc(U, n_1) \to \app \ n_1\ (n_2+n_3)\ v_1 \ (\app\ n_2\ n_3 \ v_2 \ v_3) = \app \ (n_1 + n_2) \ n_3\ (\app \ n_1 \ n_2 \ v_1 \ v_2) \ v_3)$. 
  
  \noindent Let $P:= \iota (y;z). (\app \ z\ (n_2+n_3)\ y \ (\app\ n_2\ n_3 \ v_2 \ v_3) = \app \ (z + n_2) \ n_3\ (\app \ z \ n_2 \ y \ v_2) \ v_3)$. We instantiate the $C$ in $\mathsf{Ind}(U,n_1)$ with $P$, by comprehension we have 
  
\noindent $(\forall y. \forall m. \forall u. (m\ep \mathsf{Nat} \to u \ep U \to (y;m) \ep P  \to (\mathsf{cons}\ m\ u\ y; \mathsf{S}m) \ep P )) \to (\mathsf{nil}; 0) \ep P \to \forall l.( l\ep \vecc(U,n) \to (l; n) \ep P)$. 
  
  \noindent So we just need to prove base case: 
  
  $\app \ 0\ (n_2+n_3)\ \nil \ (\app\ n_2\ n_3 \ v_2 \ v_3) = \app \ (0 + n_2) \ n_3\ (\app \ 0 \ n_2 \ \nil \ v_2) \ v_3$
  
  \noindent and step case:
  
  $\forall y. \forall m. \forall u.(m\ep \mathsf{Nat} \to u \ep U\to  (\app \ m\ (n_2+n_3)\ y \ (\app\ n_2\ n_3 \ v_2 \ v_3) = \app \ (m + n_2) \ n_3\ (\app \ m \ n_2 \ y \ v_2) \ v_3)\to (\app \ \suc m\ (n_2+n_3)\ (\mathsf{cons}\ m\ u\ y) \ (\app\ n_2\ n_3 \ v_2 \ v_3) = \app \ (\suc m + n_2) \ n_3\ (\app \ \suc m \ n_2 \ (\mathsf{cons}\ m\ u\ y) \ v_2) \ v_3))$. 
  
  \noindent For the base case, $\app \ 0\ (n_2+n_3)\ \nil \ (\app\ n_2\ n_3 \ v_2 \ v_3) \to_{\beta}^* \app\ n_2\ n_3 \ v_2 \ v_3 \leftarrow_{\beta}^* \app \ (0 + n_2) \ n_3\ (\app \ 0 \ n_2 \ \nil \ v_2) \ v_3$. For the step case, we assume $\app \ m\ (n_2+n_3)\ y \ (\app\ n_2\ n_3 \ v_2 \ v_3) = \app \ (m + n_2) \ n_3\ (\app \ m \ n_2 \ y \ v_2) \ v_3$(IH), we want to show
  
\noindent  $\app \ \suc m\ (n_2+n_3)\ (\mathsf{cons}\ m\ u\ y) \ (\app\ n_2\ n_3 \ v_2 \ v_3) = $
  
  \noindent $\app \ (\suc m + n_2) \ n_3\ (\app \ \suc m \ n_2 \ (\mathsf{cons}\ m\ u\ y) \ v_2) \ v_3$(Goal). 
  
  \noindent We know that 
  
  \noindent $\app \ \suc m\ (n_2+n_3)\ (\mathsf{cons}\ m\ u\ y) \ (\app\ n_2\ n_3 \ v_2 \ v_3) \to_{\beta}^* \cons (m+n_2+n_3)\ u \ \gray{$(\app \ m\ (n_2 + n_3)\ y \ (\app\ n_2 \ n_3\ v_2 \ v_3))$}$. The right hand side of the (Goal) can be reduced to $\cons (m+n_2+n_3)\ u \gray{$(\app \ (m+n_2)\ n_3\ (\app \ m \ n_2\ y\ v_2)\ v_3)$}$. So (IH) is enough to give us the (goal).
\end{proof}

\section{Summary}
We present System $\systemg$, which is suitable to serve as a foundational system for both formalize mathematics and reasoning about programs. We develop Peano's axioms and Vector encoding
in System $\systemg$ as evidents for its potentials. The usefulness of $\systemg \lbrack t \rbrack$ is not obvious in this chapter. However, if we switch the data-type encoding to Church encoding, then $\systemg \lbrack t \rbrack$ will become more useful. The existence of $\systemg \lbrack t \rbrack$ shows that we can understand the phenomina of polymorphic-dependent type with
$\systemg$. It is important to note that the essential difference between System $\systemg$ and $\mathrm{PTS}$ style system is that computation at formula level is currently not possible in $\systemg$. We think that computation on formula may be better treated as external feature of a logic system instead of support it internally within the logical system. Of course, it is not a conclusive assertion, more research will be needed to explore this issue. 

When comparing to usual typed functional programming language, the set in System $\systemg$ is 
more precise than the notion of type in typed functional programming language. A direct consequence is that it is impossible to fully automate the reasoning with $\systemg$. However, a degree of automation is still possible, together with human guidence, it would be an attracting 
tool to have besides the usual type system. Again, we would have to leave this to future research to see whether if it is feasible to incorporate System $\systemg$ into a typed functional programming language.  

\bibliographystyle{plain}

% The bibliography should be embedded for final submission.
\bibliography{comprehension}


\end{document}
